\begin{tabbing}
$\vdash$  \=$\forall$$A$, $B$:Type, $f$:($A$$\rightarrow$($B$ + Top)), $P$:($A$$\rightarrow\mathbb{P}$), $p$:($\forall$$x$:$A$. Dec($P$($x$))), $x$:$A$.\+
\\[0ex]($\uparrow$can{-}apply(p{-}restrict($f$;$p$);$x$)) $\Leftarrow\!\Rightarrow$ (($\uparrow$can{-}apply($f$;$x$)) \& $P$($x$))
\-
\end{tabbing}